nLab modal hyperdoctrine

Idea

A modal hyperdoctrine is a framework for modal logic in the presence of different contexts.

It is an hyperdoctrine that is equipped with a compatible modal operator, often a compatible closure operator, hence a universal closure operator.

Related concepts

• modal type theory

References

Around p. 597 of

• P. Blacksburn, J. van Benthem, F. Wolter, Handbook of modal logic, Studies in Logic and Practical reasoning volume 3 (2007)

p. 43 of

• M. Kracht, O. Kutz, Logically Possible Worlds and Counterpart Semantics for Modal Logic, (pdf)